\begin{tabbing}
R{-}Feasible\=\{i:l\}\+
\\[0ex](Rplus(\=ecl{-}machine\=\{ecl:ut2\}\+\+
\\[0ex](\=mkid\{b:ut2\};\+
\\[0ex]fpf{-}single(mkid\{x:ut2\}; $\mathbb{Z}$);
\\[0ex]fpf{-}join(\=Kind{-}deq;\+
\\[0ex]fpf{-}join(\=Kind{-}deq;\+
\\[0ex]fpf{-}single(\=rcv(mklnk\{\=a:ut2, b:ut2, 1:ut2\+\+
\\[0ex]\},mkid\{x:ut2\});
\-\\[0ex]$\mathbb{Z}$);
\-\\[0ex]fpf{-}single(\=rcv(mklnk\{\=a:ut2, b:ut2, 1:ut2\+\+
\\[0ex]\},mkid\{y:ut2\});
\-\\[0ex]$\mathbb{Z}$));
\-\-\\[0ex]fpf{-}single(\=rcv(mklnk\{\=b:ut2, output:ut2, 1:ut2\+\+
\\[0ex]\},mkid\{hello:ut2\});
\-\\[0ex]$\mathbb{B}$));
\-\-\\[0ex]eclseq(\=eclact(\=eclbase(\=rcv(mklnk\{\=a:ut2, b:ut2, 1:ut2\+\+\+\+
\\[0ex]\},mkid\{x:ut2\});
\-\\[0ex]($\lambda$$s$,$v$. ($s$(mkid\{x:ut2\})) $<$z $v$));
\-\\[0ex]1);
\-\\[0ex]eclact(\=eclbase(\=rcv(mklnk\{\=a:ut2, b:ut2, 1:ut2\+\+\+
\\[0ex]\},mkid\{y:ut2\});
\-\\[0ex]($\lambda$$s$,$v$. $v$ $<$z ($s$(mkid\{x:ut2\}))));
\-\\[0ex]2));
\-\-\\[0ex]msg{-}spec1(\=rcv(mklnk\{a:ut2, b:ut2, 1:ut2\},mkid\{y:ut2\});\+
\\[0ex]mklnk\{b:ut2, output:ut2, 1:ut2\};
\\[0ex]mkid\{hello:ut2\};
\\[0ex]2;
\\[0ex]$s$,$v$.tt);
\-\\[0ex]update{-}spec{-}join(\=update{-}spec1(\=rcv(mklnk\{\=a:ut2, b:ut2, 1:ut2\+\+\+
\\[0ex]\},mkid\{x:ut2\});
\-\\[0ex]mkid\{x:ut2\};
\\[0ex]1;
\\[0ex]$s$,$v$.$v$);
\-\\[0ex]update{-}spec1(\=rcv(mklnk\{\=a:ut2, b:ut2, 1:ut2\+\+
\\[0ex]\},mkid\{y:ut2\});
\-\\[0ex]mkid\{x:ut2\};
\\[0ex]2;
\\[0ex]$s$,$v$.$v$)));
\-\-\-\-\\[0ex]Rplus(\=Rpre(\=mkid\{a:ut2\};\+\+
\\[0ex]fpf{-}single(mkid\{x:ut2\}; $\mathbb{Z}$);
\\[0ex]mkid\{a:ut2\};
\\[0ex]unit{-}fps;
\\[0ex]($\lambda$$s$.($s$(mkid\{x:ut2\})) $<$z 10));
\-\\[0ex]Rplus(\=Reffect(\=mkid\{a:ut2\};\+\+
\\[0ex]fpf{-}single(mkid\{x:ut2\}; $\mathbb{Z}$);
\\[0ex]locl(mkid\{a:ut2\});
\\[0ex]p{-}outcome(unit{-}fps);
\\[0ex]mkid\{x:ut2\};
\\[0ex](inl ($\lambda$$s$,$v$. ($s$(mkid\{x:ut2\})) + 1) ));
\-\\[0ex]Rplus(\=Rsends(\=fpf{-}single(mkid\{x:ut2\}; $\mathbb{Z}$);\+\+
\\[0ex]locl(mkid\{a:ut2\});
\\[0ex]p{-}outcome(unit{-}fps);
\\[0ex]mklnk\{a:ut2, b:ut2, 1:ut2\};
\\[0ex]fpf{-}single(mkid\{x:ut2\}; $\mathbb{Z}$);
\\[0ex]cons(\=$<$mkid\{x:ut2\}\+
\\[0ex], $\lambda$$s$,$v$. cons(($s$(mkid\{x:ut2\})); [])
\\[0ex]$>$;
\\[0ex][]));
\-\-\\[0ex]Rplus(\=Rsends(\=fpf{-}empty;\+\+
\\[0ex]rcv(mklnk\{\=input:ut2, a:ut2, 1:ut2\+
\\[0ex]\},mkid\{key:ut2\});
\-\\[0ex]$\mathbb{Z}$;
\\[0ex]mklnk\{a:ut2, b:ut2, 1:ut2\};
\\[0ex]fpf{-}single(mkid\{y:ut2\}; $\mathbb{Z}$);
\\[0ex]cons($<$mkid\{y:ut2\}, $\lambda$$s$,$v$. cons($v$; [])$>$; [])
\\[0ex]);
\-\\[0ex]Rplus(\=Rsends(\=fpf{-}empty;\+\+
\\[0ex]rcv(mklnk\{\=input:ut2, a:ut2, 1:ut2\+
\\[0ex]\},mkid\{string:ut2\});
\-\\[0ex]atom;
\\[0ex]mklnk\{a:ut2, b:ut2, 1:ut2\};
\\[0ex]fpf{-}single(mkid\{string:ut2\}; atom);
\\[0ex]cons(\=$<$mkid\{string:ut2\}\+
\\[0ex], $\lambda$$s$,$v$. cons($v$; [])
\\[0ex]$>$;
\\[0ex][]));
\-\-\\[0ex]Rplus(\=Rsends(\=fpf{-}empty;\+\+
\\[0ex]rcv(mklnk\{\=input:ut2,\+
\\[0ex]a:ut2,
\\[0ex]1:ut2\},mkid\{b:ut2\});
\-\\[0ex]$\mathbb{B}$;
\\[0ex]mklnk\{a:ut2, b:ut2, 1:ut2\};
\\[0ex]fpf{-}single(mkid\{b:ut2\}; $\mathbb{B}$);
\\[0ex]cons(\=$<$mkid\{b:ut2\}\+
\\[0ex], $\lambda$$s$,$v$. cons($v$; [])
\\[0ex]$>$;
\\[0ex][]));
\-\-\\[0ex]Rsends(\=fpf{-}empty;\+
\\[0ex]rcv(mklnk\{\=input:ut2,\+
\\[0ex]a:ut2,
\\[0ex]1:ut2
\\[0ex]\},mkid\{hello:ut2\});
\-\\[0ex]Unit;
\\[0ex]mklnk\{a:ut2, b:ut2, 1:ut2\};
\\[0ex]fpf{-}single(\=mkid\{hello:ut2\};\+
\\[0ex]Unit);
\-\\[0ex]cons(\=$<$mkid\{hello:ut2\}\+
\\[0ex], $\lambda$$s$,$v$. cons($v$; [])
\\[0ex]$>$;
\\[0ex][]))))))))))
\-\-\-\-\-\-\-\-\-\-
\end{tabbing}